COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 know4.lsp[f81,jmc]	comments and axioms on Kripke type knowledge
C00004 ENDMK
C⊗;
;;; know4.lsp[f81,jmc]	comments and axioms on Kripke type knowledge

;;; To say that  s  knows exactly  baz  and whether  p, we write

∀w1.a(w,w1,s) ⊃ baz(w1) = baz(w) ∧ (p(w1) ≡ p(w)) ∧
∀x.baz(w) = x ⊃ ∃w1.a(w,w1,s) ∧ baz(w1)=x ∧ (p(w1) ≡ p(w))

;;; To say that  s  knows exactly  foo  and  baz, we
;;; define  mumph(w) = cons(foo(w),baz(w))

dec 7

(declare knowledge |person⊗world→(world→truthval)| constant)

To say that a person knows exactly  p  we can write

s knows exactly p in w at time  t  if
∃w1.p(w1)∧q(w1) ≡ ∃w1.a(w,w1,s,t)∧p(w1)∧q(w1)

or in a modal form

S knows exactly p ≡ S knows p ∧ ∀q.possible(p∧q) ⊃ possible for S (p∧q)

So the problem reduces to that of formalizing what is a priori possible.